Section: Partnerships and Cooperations

National Initiatives

ANR

AnaStaSec

• Title: Static Analysis for Security Properties (ANR générique 2014.)

• Other partners: Inria Paris/EPI Antique, Inria Rennes/EPI Celtique, Airbus Operations SAS, AMOSSYS, CEA-LIST, TrustInSoft

• Duration: January 2015 - September 2019.

• Coordinator: Jérôme Féret, EPI Antique, Inria Paris (France)

• Participant: Bruno Blanchet

• Abstract: The project aims at using automated static analysis techniques for verifying security and confidentiality properties of critical avionics software.

AJACS

• Title: AJACS: Analyses of JavaScript Applications: Certification and Security

• Other partners: Inria-Rennes/Celtique, Inria-Saclay/Toccata, Inria-Sophia Antipolis/INDES, Imperial College London

• Duration: October 2014 - March 2019.

• Coordinator: Alan Schmitt, Inria (France)

• Participants: Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi

• Abstract: The goal of the AJACS project is to provide strong security and privacy guarantees for web application scripts. To this end, we propose to define a mechanized semantics of the full JavaScript language, the most widely used language for the Web, to develop and prove correct analyses for JavaScript programs, and to design and certify security and privacy enforcement mechanisms.

SafeTLS

• Title: SafeTLS: La sécurisation de l'Internet du futur avec TLS 1.

• Other partners: Université Rennes 1, IRMAR, Inria Sophia Antipolis, SGDSN/ANSSI

• Duration: October 2016 - September 2020

• Coordinator: Pierre-Alain Fouque, Université de Rennes 1 (France)

• Participants: Karthikeyan Bhargavan

• Abstract: Our project, SafeTLS, addresses the security of both TLS 1.3 and of TLS 1.2 as they are (expected to be) used, in three important ways: (1) A better understanding: We will provide a better understanding of how TLS 1.2 and 1.3 are used in real-world applications; (2) Empowering clients: By developing a tool that will show clients the quality of their TLS connection and inform them of potential security and privacy risks; (3) Analyzing implementations: We will analyze the soundness of current TLS 1.2 implementations and use automated verification to provide a backbone of a secure TLS 1.3 implementation.

TECAP

• Title: TECAP: Protocol Analysis - Combining Existing Tools (ANR générique 2017.)

• Other partners: Inria Nancy/EPI PESTO, Inria Sophia Antipolis/EPI MARELLE, IRISA, LIX, LSV - ENS Cachan.

• Duration: January 2018 - December 20

• Coordinator: Vincent Cheval, EPI PESTO, Inria Nancy (France)

• Participants: Bruno Blanchet, Benjamin Lipp

• Abstract: A large variety of automated verification tools have been developed to prove or find attacks on security protocols. These tools differ in their scope, degree of automation, and attacker models. The aim of this project is to get the best of all these tools, meaning, on the one hand, to improve the theory and implementations of each individual tool towards the strengths of the others and, on the other hand, build bridges that allow the cooperations of the methods/tools. We will focus in this project on the tools CryptoVerif, EasyCrypt, Scary, ProVerif, Tamarin, AKiSs and APTE.